(set-logic QF_ABV)
(set-option :smt.dack.eq true)
(set-option :smt.phase_selection 1)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const arr-4113461120939453771_-1502630483009269712-0 (Array (_ BitVec 10) Bool))
(declare-const v11 Bool)
(declare-const arr-4113461120939453771_4113461120939453771-0 (Array (_ BitVec 10) (_ BitVec 10)))
(declare-const v12 Bool)
(declare-const arr-4113461120939453771_4113461120939453771-2 (Array (_ BitVec 10) (_ BitVec 10)))
(declare-const v13 Bool)
(declare-const arr-4113461120939453771_4113461120939453771-4 (Array (_ BitVec 10) (_ BitVec 10)))
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const arr-4113461120934041146_4113461120939453771-0 (Array (_ BitVec 17) (_ BitVec 10)))
(declare-const arr-4113461120939453771_-6079933644237103909-0 (Array (_ BitVec 10) (Array (_ BitVec 10) Bool)))
(declare-const v17 Bool)
(declare-const bv_30-0 (_ BitVec 30))
(assert (or v15 v17 (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103))))
(assert (or v5 (not (xor v3 v7 v1 v4 v4 v8 v8)) (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))))
(assert (or (= (_ bv997 10) #b0111010001 (bvshl #b0111010001 #b0111010001) #b0111010001) v2 (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))))
(assert (or v1 (= (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) #x103 #x103 (bvlshr #x103 #x103)) v15))
(assert (or v1 v1 v9))
(assert (or (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7)) v14 v17))
(assert (or (not v9) (not (xor v3 v7 v1 v4 v4 v8 v8)) (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103))))
(assert (or (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7)) (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))))
(assert (or (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7)) (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))))
(assert (or (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103)) (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7)) v11))
(assert (or (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v8 v1))
(assert (or v8 v14 v1))
(assert (or v5 v11 v15))
(assert (or v17 (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))))
(assert (or v9 (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7)) v2))
(assert (or v1 v2 v1))
(assert (or (= (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) #x103 #x103 (bvlshr #x103 #x103)) v1 (= (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) #x103 #x103 (bvlshr #x103 #x103))))
(assert (or v15 (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7)) v1))
(assert (or (not v9) v5 (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7))))
(assert (or v9 (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v1))
(assert (or (not v9) (not (xor v3 v7 v1 v4 v4 v8 v8)) v14))
(assert (or v11 v17 v15))
(assert (or (xor v3 v7 v1 v4 v4 v8 v8) (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v9))
(assert (or v15 (not (xor v3 v7 v1 v4 v4 v8 v8)) (bvugt #b0111010001 #b0111010001)))
(assert (or (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v9 (= (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) #x103 #x103 (bvlshr #x103 #x103))))
(assert (or v15 (not (xor v3 v7 v1 v4 v4 v8 v8)) (= (_ bv997 10) #b0111010001 (bvshl #b0111010001 #b0111010001) #b0111010001)))
(assert (or (= (_ bv997 10) #b0111010001 (bvshl #b0111010001 #b0111010001) #b0111010001) (not (xor v3 v7 v1 v4 v4 v8 v8)) v14))
(assert (or v8 v14 v11))
(assert (or (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7)) v14 (= (_ bv997 10) #b0111010001 (bvshl #b0111010001 #b0111010001) #b0111010001)))
(assert (or (not v9) v11 (bvugt #b0111010001 #b0111010001)))
(assert (or (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103)) (not v9) v1))
(assert (or v15 (not v9) (= (_ bv997 10) #b0111010001 (bvshl #b0111010001 #b0111010001) #b0111010001)))
(assert (or (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v8 (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))))
(assert (or (not (xor v3 v7 v1 v4 v4 v8 v8)) (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103)) (= (_ bv997 10) #b0111010001 (bvshl #b0111010001 #b0111010001) #b0111010001)))
(assert (or (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103)) (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7)) v11))
(assert (or v11 (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v5))
(assert (or (xor v3 v7 v1 v4 v4 v8 v8) v9 (not (xor v3 v7 v1 v4 v4 v8 v8))))
(assert (or (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103)) v11 v15))
(assert (or v11 v8 (xor v3 v7 v1 v4 v4 v8 v8)))
(assert (or v15 (= (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) #x103 #x103 (bvlshr #x103 #x103)) v8))
(assert (or (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103)) (not v9) v5))
(assert (or v9 (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v9))
(assert (or (bvugt #b0111010001 #b0111010001) (= (_ bv997 10) #b0111010001 (bvshl #b0111010001 #b0111010001) #b0111010001) v15))
(assert (or v1 v8 v14))
(assert (or v15 (not (xor v3 v7 v1 v4 v4 v8 v8)) (not v9)))
(assert (or (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) (= (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) #x103 #x103 (bvlshr #x103 #x103)) v5))
(assert (or v2 (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) (= (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) #x103 #x103 (bvlshr #x103 #x103))))
(assert (or v9 (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v9))
(assert (or v15 (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103)) (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))))
(assert (or (not (xor v3 v7 v1 v4 v4 v8 v8)) v2 (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))))
(assert (or (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7)) (xor v3 v7 v1 v4 v4 v8 v8) (xor v3 v7 v1 v4 v4 v8 v8)))
(assert (or (bvugt #b0111010001 #b0111010001) (not (xor v3 v7 v1 v4 v4 v8 v8)) (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))))
(assert (or (xor v3 v7 v1 v4 v4 v8 v8) (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) (not v9)))
(assert (or v5 v5 (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))))
(assert (or v2 v15 (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7))))
(assert (or v8 (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v11))
(assert (or (= (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) #x103 #x103 (bvlshr #x103 #x103)) v2 v8))
(assert (or v11 (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v5))
(assert (or (= (_ bv997 10) #b0111010001 (bvshl #b0111010001 #b0111010001) #b0111010001) (not (xor v3 v7 v1 v4 v4 v8 v8)) v14))
(assert (and (or (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7)) (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))) (or v11 v17 v15) (or (= (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) #x103 #x103 (bvlshr #x103 #x103)) v2 v8) (or (= (_ bv997 10) #b0111010001 (bvshl #b0111010001 #b0111010001) #b0111010001) v2 (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))) (or v5 (not (xor v3 v7 v1 v4 v4 v8 v8)) (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))) (or v1 v8 v14) (and (or v15 (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103)) (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))) (or (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v8 (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))) (or (xor v3 v7 v1 v4 v4 v8 v8) (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v9) (or (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103)) (not v9) v1) (or (not v9) v5 (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7))) (or (xor v3 v7 v1 v4 v4 v8 v8) v9 (not (xor v3 v7 v1 v4 v4 v8 v8))) (or (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) (= (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) #x103 #x103 (bvlshr #x103 #x103)) v5) (or (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103)) v11 v15) (or v5 (not (xor v3 v7 v1 v4 v4 v8 v8)) (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))))) (or v11 v17 v15) (or v5 v11 v15)))
(assert (=> (or (= (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) #x103 #x103 (bvlshr #x103 #x103)) v2 v8) (or (not (xor v3 v7 v1 v4 v4 v8 v8)) (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103)) (= (_ bv997 10) #b0111010001 (bvshl #b0111010001 #b0111010001) #b0111010001))))
(assert (or (or v1 v1 v9) (or (not v9) (not (xor v3 v7 v1 v4 v4 v8 v8)) (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103)))))
(assert (or (or (not (xor v3 v7 v1 v4 v4 v8 v8)) v2 (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))) (or (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7)) (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))) (or (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) (= (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) #x103 #x103 (bvlshr #x103 #x103)) v5) (or v9 (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v9)))
(assert (or (or v2 (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) (= (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) #x103 #x103 (bvlshr #x103 #x103))) (or (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7)) v14 (= (_ bv997 10) #b0111010001 (bvshl #b0111010001 #b0111010001) #b0111010001)) (or v8 v14 v1) (or v15 (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7)) v1) (or v5 v5 (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))) (or v1 v8 v14) (or v2 v15 (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7))) (or v11 v8 (xor v3 v7 v1 v4 v4 v8 v8)) (or v2 (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) (= (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) #x103 #x103 (bvlshr #x103 #x103))) (or v8 (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v11)))
(assert (=> (or v8 (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v11) (or (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7)) (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))))))
(assert (or (or (not (xor v3 v7 v1 v4 v4 v8 v8)) (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103)) (= (_ bv997 10) #b0111010001 (bvshl #b0111010001 #b0111010001) #b0111010001)) (or (xor v3 v7 v1 v4 v4 v8 v8) (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v9)))
(assert (or (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v8 v1))
(assert (=> (or (bvugt #b0111010001 #b0111010001) (= (_ bv997 10) #b0111010001 (bvshl #b0111010001 #b0111010001) #b0111010001) v15) (or (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7)) v14 (= (_ bv997 10) #b0111010001 (bvshl #b0111010001 #b0111010001) #b0111010001))))
(assert (or (or (or (not (xor v3 v7 v1 v4 v4 v8 v8)) (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103)) (= (_ bv997 10) #b0111010001 (bvshl #b0111010001 #b0111010001) #b0111010001)) (or (xor v3 v7 v1 v4 v4 v8 v8) (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v9)) (or v15 (not (xor v3 v7 v1 v4 v4 v8 v8)) (bvugt #b0111010001 #b0111010001))))
(assert (or (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103)) (not v9) v5))
(assert (or v9 (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v1))
(assert (or (or v8 v14 v1) (or v17 (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))) (or (= (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) #x103 #x103 (bvlshr #x103 #x103)) v1 (= (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) #x103 #x103 (bvlshr #x103 #x103))) (and (or v15 (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103)) (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))) (or (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v8 (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))) (or (xor v3 v7 v1 v4 v4 v8 v8) (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) v9) (or (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103)) (not v9) v1) (or (not v9) v5 (not (and v0 v4 v4 v1 v2 v2 (= v9 v10 (bvugt #b0111010001 #b0111010001) v10) v11 v0 v7))) (or (xor v3 v7 v1 v4 v4 v8 v8) v9 (not (xor v3 v7 v1 v4 v4 v8 v8))) (or (= (_ bv997 10) (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10))) (= (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) #x103 #x103 (bvlshr #x103 #x103)) v5) (or (= #x103 (bvlshr #x103 #x103) (bvlshr #x103 #x103) (bvmul (bvlshr #x103 #x103) (bvlshr #x103 #x103)) (bvlshr #x103 #x103)) v11 v15) (or v5 (not (xor v3 v7 v1 v4 v4 v8 v8)) (distinct arr-4113461120939453771_4113461120939453771-0 (store arr-4113461120939453771_4113461120939453771-0 (bvudiv #b0111010001 (bvshl #b0111010001 #b0111010001)) (bvshl #b0111010001 #b0111010001)) (store arr-4113461120939453771_4113461120939453771-2 (_ bv997 10) (_ bv997 10)) (store arr-4113461120939453771_4113461120939453771-2 (bvmul #b0111010001 (bvshl #b0111010001 #b0111010001)) (_ bv997 10)))))))
(minimize bv_30-0)
(check-sat)
(exit)
